고정점 조합자

고정점 조합자(fixpoint combinator)는 λ-계산등에서 임의의 함수의 고정점을 주는 조합자이다.

목록

Y 조합자

Y 조합자는 타입 없는 λ-계산의 대표적인 고정점 조합자이다.

\[ Y = \lambda f. (\lambda x. f(xx)) (\lambda x. f(xx)) \]

다음의 두 계산으로 임의의 항 \(f\)에 대해 \(Yf\)와 \(f(Yf)\)가 β-동치임을 알 수 있다. \[ \begin{array}{rcl} Yf &= & (\lambda f. (\lambda x. f(xx)) (\lambda x. f(xx))) f \\ &\longrightarrow & (\lambda x. f(xx)) (\lambda x. f(xx)) \\ &\longrightarrow & f ((\lambda x. f(xx)) (\lambda x. f(xx))) \end{array} \] \[ \begin{array}{rcl} f(Yf) &= & f ((\lambda f. (\lambda x. f(xx)) (\lambda x. f(xx))) f) \\ &\longrightarrow & f ((\lambda x. f(xx)) (\lambda x. f(xx))) \\ \end{array} \]

Θ 조합자

Y 조합자는 임의의 항 \(f\)에 대해 \(Yf\)와 \(f(Yf)\)가 β-동치이긴 하지만, \(Yf\)가 \(f(Yf)\)로 축약되지는 않는다. 반면에 튜링의 Θ 조합자는 \(\Theta f\)가 직접 \(f(\Theta f)\)로 축약되는 특징이 있다.

\[ \Theta = (\lambda x y. y(xxy)) (\lambda x y. y(xxy)) \]

\[ \begin{array}{rcl} \Theta f &= & (\lambda x y. y(xxy)) (\lambda x y. y(xxy)) f \\ &\longrightarrow & (\lambda y. y((\lambda x y. y(xxy))(\lambda x y. y(xxy))y)) f \\ &\longrightarrow & f ((\lambda x y. y(xxy))(\lambda x y. y(xxy)) f) \\ &= & f (\Theta f) \end{array} \]

Z 조합자

Y 조합자가 쓰인 식을 call-by-value로 축약 하는 경우, 정규형이 존재함에도 정지하지 않을 수 있다. Z 조합자는 Y 조합자와 달리 이런 단점이 없다.

\[ Z = \lambda f. (\lambda x. f(\lambda v. xxv)) (\lambda x. f(\lambda v. xxv))\]